plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
↳ QTRS
↳ Overlay + Local Confluence
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
TOWERITER(s(x), y, z) → P(s(x))
TOWERITER(s(x), y, z) → TOWERITER(p(s(x)), y, exp(y, z))
PLUS(s(x), y) → PLUS(p(s(x)), y)
PLUS(s(x), y) → P(s(x))
P(s(s(x))) → P(s(x))
TOWER(x, y) → TOWERITER(x, y, s(0))
TIMES(s(x), y) → TIMES(p(s(x)), y)
TIMES(s(x), y) → P(s(x))
TOWERITER(s(x), y, z) → EXP(y, z)
EXP(x, s(y)) → EXP(x, y)
EXP(x, s(y)) → TIMES(x, exp(x, y))
TIMES(s(x), y) → PLUS(y, times(p(s(x)), y))
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
TOWERITER(s(x), y, z) → P(s(x))
TOWERITER(s(x), y, z) → TOWERITER(p(s(x)), y, exp(y, z))
PLUS(s(x), y) → PLUS(p(s(x)), y)
PLUS(s(x), y) → P(s(x))
P(s(s(x))) → P(s(x))
TOWER(x, y) → TOWERITER(x, y, s(0))
TIMES(s(x), y) → TIMES(p(s(x)), y)
TIMES(s(x), y) → P(s(x))
TOWERITER(s(x), y, z) → EXP(y, z)
EXP(x, s(y)) → EXP(x, y)
EXP(x, s(y)) → TIMES(x, exp(x, y))
TIMES(s(x), y) → PLUS(y, times(p(s(x)), y))
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
TOWERITER(s(x), y, z) → P(s(x))
PLUS(s(x), y) → PLUS(p(s(x)), y)
TOWERITER(s(x), y, z) → TOWERITER(p(s(x)), y, exp(y, z))
PLUS(s(x), y) → P(s(x))
TOWER(x, y) → TOWERITER(x, y, s(0))
TIMES(s(x), y) → P(s(x))
EXP(x, s(y)) → TIMES(x, exp(x, y))
TOWERITER(s(x), y, z) → EXP(y, z)
P(s(s(x))) → P(s(x))
TIMES(s(x), y) → TIMES(p(s(x)), y)
EXP(x, s(y)) → EXP(x, y)
TIMES(s(x), y) → PLUS(y, times(p(s(x)), y))
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
P(s(s(x))) → P(s(x))
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(s(s(x))) → P(s(x))
[P1, s1]
P1: multiset
s1: multiset
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS(s(x), y) → PLUS(p(s(x)), y)
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
TIMES(s(x), y) → TIMES(p(s(x)), y)
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
EXP(x, s(y)) → EXP(x, y)
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EXP(x, s(y)) → EXP(x, y)
[EXP2, s1]
EXP2: multiset
s1: [1]
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
TOWERITER(s(x), y, z) → TOWERITER(p(s(x)), y, exp(y, z))
plus(0, x) → x
plus(s(x), y) → s(plus(p(s(x)), y))
times(0, y) → 0
times(s(x), y) → plus(y, times(p(s(x)), y))
exp(x, 0) → s(0)
exp(x, s(y)) → times(x, exp(x, y))
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
tower(x, y) → towerIter(x, y, s(0))
towerIter(0, y, z) → z
towerIter(s(x), y, z) → towerIter(p(s(x)), y, exp(y, z))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
exp(x0, 0)
exp(x0, s(x1))
p(s(0))
p(s(s(x0)))
tower(x0, x1)
towerIter(0, x0, x1)
towerIter(s(x0), x1, x2)